0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 82 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 69 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇒, 47 ms)
↳8 QDP
↳9 MRRProof (⇔, 240 ms)
↳10 QDP
↳11 PisEmptyProof (⇔, 0 ms)
↳12 YES
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U1_GA(X1, X2, X3, hbal_treeA_in_ga(s(X1), X2))
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → HBAL_TREEA_IN_GA(s(X1), X2)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U2_GA(X1, X2, X3, hbal_treecA_in_ga(s(X1), X2))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U3_GA(X1, X2, X3, hbal_treeA_in_ga(s(X1), X3))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(s(X1), X3)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U5_GA(X1, X2, X3, hbal_treeA_in_ga(X1, X2))
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → HBAL_TREEA_IN_GA(X1, X2)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U6_GA(X1, X2, X3, hbal_treecA_in_ga(X1, X2))
U6_GA(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → U7_GA(X1, X2, X3, hbal_treeA_in_ga(s(X1), X3))
U6_GA(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → HBAL_TREEA_IN_GA(s(X1), X3)
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U4_GA(X1, X2, X3, hbal_treeA_in_ga(X1, X3))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(X1, X3)
hbal_treecA_in_ga(zero, nil) → hbal_treecA_out_ga(zero, nil)
hbal_treecA_in_ga(s(zero), t(x, nil, nil)) → hbal_treecA_out_ga(s(zero), t(x, nil, nil))
hbal_treecA_in_ga(s(s(X1)), t(x, X2, X3)) → U9_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X2))
hbal_treecA_in_ga(s(s(X1)), t(x, X2, X3)) → U12_ga(X1, X2, X3, hbal_treecA_in_ga(X1, X2))
U12_ga(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → U13_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X3))
U13_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U10_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X3))
U10_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U11_ga(X1, X2, X3, hbal_treecA_in_ga(X1, X3))
U11_ga(X1, X2, X3, hbal_treecA_out_ga(X1, X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U1_GA(X1, X2, X3, hbal_treeA_in_ga(s(X1), X2))
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → HBAL_TREEA_IN_GA(s(X1), X2)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U2_GA(X1, X2, X3, hbal_treecA_in_ga(s(X1), X2))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U3_GA(X1, X2, X3, hbal_treeA_in_ga(s(X1), X3))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(s(X1), X3)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U5_GA(X1, X2, X3, hbal_treeA_in_ga(X1, X2))
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → HBAL_TREEA_IN_GA(X1, X2)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U6_GA(X1, X2, X3, hbal_treecA_in_ga(X1, X2))
U6_GA(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → U7_GA(X1, X2, X3, hbal_treeA_in_ga(s(X1), X3))
U6_GA(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → HBAL_TREEA_IN_GA(s(X1), X3)
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U4_GA(X1, X2, X3, hbal_treeA_in_ga(X1, X3))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(X1, X3)
hbal_treecA_in_ga(zero, nil) → hbal_treecA_out_ga(zero, nil)
hbal_treecA_in_ga(s(zero), t(x, nil, nil)) → hbal_treecA_out_ga(s(zero), t(x, nil, nil))
hbal_treecA_in_ga(s(s(X1)), t(x, X2, X3)) → U9_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X2))
hbal_treecA_in_ga(s(s(X1)), t(x, X2, X3)) → U12_ga(X1, X2, X3, hbal_treecA_in_ga(X1, X2))
U12_ga(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → U13_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X3))
U13_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U10_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X3))
U10_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U11_ga(X1, X2, X3, hbal_treecA_in_ga(X1, X3))
U11_ga(X1, X2, X3, hbal_treecA_out_ga(X1, X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U2_GA(X1, X2, X3, hbal_treecA_in_ga(s(X1), X2))
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(s(X1), X3)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → HBAL_TREEA_IN_GA(s(X1), X2)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → HBAL_TREEA_IN_GA(X1, X2)
HBAL_TREEA_IN_GA(s(s(X1)), t(x, X2, X3)) → U6_GA(X1, X2, X3, hbal_treecA_in_ga(X1, X2))
U6_GA(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → HBAL_TREEA_IN_GA(s(X1), X3)
U2_GA(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(X1, X3)
hbal_treecA_in_ga(zero, nil) → hbal_treecA_out_ga(zero, nil)
hbal_treecA_in_ga(s(zero), t(x, nil, nil)) → hbal_treecA_out_ga(s(zero), t(x, nil, nil))
hbal_treecA_in_ga(s(s(X1)), t(x, X2, X3)) → U9_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X2))
hbal_treecA_in_ga(s(s(X1)), t(x, X2, X3)) → U12_ga(X1, X2, X3, hbal_treecA_in_ga(X1, X2))
U12_ga(X1, X2, X3, hbal_treecA_out_ga(X1, X2)) → U13_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X3))
U13_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U10_ga(X1, X2, X3, hbal_treecA_in_ga(s(X1), X3))
U10_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, X2, X3, hbal_treecA_out_ga(s(X1), X2)) → U11_ga(X1, X2, X3, hbal_treecA_in_ga(X1, X3))
U11_ga(X1, X2, X3, hbal_treecA_out_ga(X1, X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
HBAL_TREEA_IN_GA(s(s(X1))) → U2_GA(X1, hbal_treecA_in_ga(s(X1)))
U2_GA(X1, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(s(X1))
HBAL_TREEA_IN_GA(s(s(X1))) → HBAL_TREEA_IN_GA(s(X1))
HBAL_TREEA_IN_GA(s(s(X1))) → HBAL_TREEA_IN_GA(X1)
HBAL_TREEA_IN_GA(s(s(X1))) → U6_GA(X1, hbal_treecA_in_ga(X1))
U6_GA(X1, hbal_treecA_out_ga(X1, X2)) → HBAL_TREEA_IN_GA(s(X1))
U2_GA(X1, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(X1)
hbal_treecA_in_ga(zero) → hbal_treecA_out_ga(zero, nil)
hbal_treecA_in_ga(s(zero)) → hbal_treecA_out_ga(s(zero), t(x, nil, nil))
hbal_treecA_in_ga(s(s(X1))) → U9_ga(X1, hbal_treecA_in_ga(s(X1)))
hbal_treecA_in_ga(s(s(X1))) → U12_ga(X1, hbal_treecA_in_ga(X1))
U12_ga(X1, hbal_treecA_out_ga(X1, X2)) → U13_ga(X1, X2, hbal_treecA_in_ga(s(X1)))
U13_ga(X1, X2, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, hbal_treecA_out_ga(s(X1), X2)) → U10_ga(X1, X2, hbal_treecA_in_ga(s(X1)))
U10_ga(X1, X2, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, hbal_treecA_out_ga(s(X1), X2)) → U11_ga(X1, X2, hbal_treecA_in_ga(X1))
U11_ga(X1, X2, hbal_treecA_out_ga(X1, X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
hbal_treecA_in_ga(x0)
U12_ga(x0, x1)
U13_ga(x0, x1, x2)
U9_ga(x0, x1)
U10_ga(x0, x1, x2)
U11_ga(x0, x1, x2)
HBAL_TREEA_IN_GA(s(s(X1))) → U2_GA(X1, hbal_treecA_in_ga(s(X1)))
U2_GA(X1, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(s(X1))
HBAL_TREEA_IN_GA(s(s(X1))) → HBAL_TREEA_IN_GA(s(X1))
HBAL_TREEA_IN_GA(s(s(X1))) → HBAL_TREEA_IN_GA(X1)
HBAL_TREEA_IN_GA(s(s(X1))) → U6_GA(X1, hbal_treecA_in_ga(X1))
U6_GA(X1, hbal_treecA_out_ga(X1, X2)) → HBAL_TREEA_IN_GA(s(X1))
U2_GA(X1, hbal_treecA_out_ga(s(X1), X2)) → HBAL_TREEA_IN_GA(X1)
POL(HBAL_TREEA_IN_GA(x1)) = 1 + 2·x1
POL(U10_ga(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3
POL(U11_ga(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3
POL(U12_ga(x1, x2)) = 1 + 2·x1 + 2·x2
POL(U13_ga(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3
POL(U2_GA(x1, x2)) = x1 + 2·x2
POL(U6_GA(x1, x2)) = 2·x1 + 2·x2
POL(U9_ga(x1, x2)) = 2 + 2·x1 + x2
POL(hbal_treecA_in_ga(x1)) = 2 + x1
POL(hbal_treecA_out_ga(x1, x2)) = 2 + x1 + 2·x2
POL(nil) = 0
POL(s(x1)) = 1 + 2·x1
POL(t(x1, x2, x3)) = x1 + x2 + x3
POL(x) = 0
POL(zero) = 2
hbal_treecA_in_ga(zero) → hbal_treecA_out_ga(zero, nil)
hbal_treecA_in_ga(s(zero)) → hbal_treecA_out_ga(s(zero), t(x, nil, nil))
hbal_treecA_in_ga(s(s(X1))) → U9_ga(X1, hbal_treecA_in_ga(s(X1)))
hbal_treecA_in_ga(s(s(X1))) → U12_ga(X1, hbal_treecA_in_ga(X1))
U12_ga(X1, hbal_treecA_out_ga(X1, X2)) → U13_ga(X1, X2, hbal_treecA_in_ga(s(X1)))
U13_ga(X1, X2, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, hbal_treecA_out_ga(s(X1), X2)) → U10_ga(X1, X2, hbal_treecA_in_ga(s(X1)))
U10_ga(X1, X2, hbal_treecA_out_ga(s(X1), X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
U9_ga(X1, hbal_treecA_out_ga(s(X1), X2)) → U11_ga(X1, X2, hbal_treecA_in_ga(X1))
U11_ga(X1, X2, hbal_treecA_out_ga(X1, X3)) → hbal_treecA_out_ga(s(s(X1)), t(x, X2, X3))
hbal_treecA_in_ga(x0)
U12_ga(x0, x1)
U13_ga(x0, x1, x2)
U9_ga(x0, x1)
U10_ga(x0, x1, x2)
U11_ga(x0, x1, x2)